Combining Decision Procedures for Sorted Theories
Identifieur interne : 006C25 ( Main/Exploration ); précédent : 006C24; suivant : 006C26Combining Decision Procedures for Sorted Theories
Auteurs : Cesare Tinelli [États-Unis] ; Calogero G. Zarba [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
- Wicri :
- topic : Intelligence artificielle.
English descriptors
- KwdEn :
Abstract
Abstract: The Nelson-Oppen combination method combines decision procedures for theories satisfying certain conditions into a decision procedure for their union. While the method is known to be correct in the setting of unsorted first-order logic, some current implementations of it appear in tools that use a sorted input language. So far, however, there have been no theoretical results on the correctness of the method in a sorted setting, nor is it obvious that the method in fact lifts as is to logics with sorts. To bridge this gap between the existing theoretical results and the current implementations, we extend the Nelson-Oppen method to (order-)sorted logic and prove it correct under conditions similar to the original ones. From a theoretical point of view, the extension is relevant because it provides a rigorous foundation for the application of the method in a sorted setting. From a practical point of view, the extension has the considerable added benefits that in a sorted setting the method’s preconditions become easier to satisfy in practice, and the method’s nondeterminism is generally reduced.
Url:
DOI: 10.1007/978-3-540-30227-8_53
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001E83
- to stream Istex, to step Curation: 001E58
- to stream Istex, to step Checkpoint: 001834
- to stream Main, to step Merge: 006F29
- to stream PascalFrancis, to step Corpus: 000596
- to stream PascalFrancis, to step Curation: 000442
- to stream PascalFrancis, to step Checkpoint: 000621
- to stream Main, to step Merge: 007056
- to stream Main, to step Curation: 006C25
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Combining Decision Procedures for Sorted Theories</title><author><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name></author><author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:85250E72E5E90BB262FF57FB7797C6F977DE2D6D</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1007/978-3-540-30227-8_53</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-57LVGN39-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001E83</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001E83</idno><idno type="wicri:Area/Istex/Curation">001E58</idno><idno type="wicri:Area/Istex/Checkpoint">001834</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001834</idno><idno type="wicri:doubleKey">0302-9743:2004:Tinelli C:combining:decision:procedures</idno><idno type="wicri:Area/Main/Merge">006F29</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:05-0041878</idno><idno type="wicri:Area/PascalFrancis/Corpus">000596</idno><idno type="wicri:Area/PascalFrancis/Curation">000442</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000621</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000621</idno><idno type="wicri:doubleKey">0302-9743:2004:Tinelli C:combining:decision:procedures</idno><idno type="wicri:Area/Main/Merge">007056</idno><idno type="wicri:Area/Main/Curation">006C25</idno><idno type="wicri:Area/Main/Exploration">006C25</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Combining Decision Procedures for Sorted Theories</title><author><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name><affiliation wicri:level="4"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Department of Computer Science, The University of Iowa</wicri:regionArea><placeName><settlement type="city">Iowa City</settlement><region type="state">Iowa</region></placeName><orgName type="university">Université de l'Iowa</orgName></affiliation></author><author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA and INRIA-Lorraine</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Artificial intelligence</term><term>Decision theory</term><term>First order logic</term><term>Logical programming</term><term>Non determinism</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Intelligence artificielle</term><term>Logique ordre 1</term><term>Non déterminisme</term><term>Programmation logique</term><term>Théorie décision</term></keywords><keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Intelligence artificielle</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The Nelson-Oppen combination method combines decision procedures for theories satisfying certain conditions into a decision procedure for their union. While the method is known to be correct in the setting of unsorted first-order logic, some current implementations of it appear in tools that use a sorted input language. So far, however, there have been no theoretical results on the correctness of the method in a sorted setting, nor is it obvious that the method in fact lifts as is to logics with sorts. To bridge this gap between the existing theoretical results and the current implementations, we extend the Nelson-Oppen method to (order-)sorted logic and prove it correct under conditions similar to the original ones. From a theoretical point of view, the extension is relevant because it provides a rigorous foundation for the application of the method in a sorted setting. From a practical point of view, the extension has the considerable added benefits that in a sorted setting the method’s preconditions become easier to satisfy in practice, and the method’s nondeterminism is generally reduced.</div></front></TEI><affiliations><list><country><li>France</li><li>États-Unis</li></country><region><li>Iowa</li></region><settlement><li>Iowa City</li></settlement><orgName><li>Université de l'Iowa</li></orgName></list><tree><country name="États-Unis"><region name="Iowa"><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name></region></country><country name="France"><noRegion><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006C25 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006C25 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:85250E72E5E90BB262FF57FB7797C6F977DE2D6D
|texte= Combining Decision Procedures for Sorted Theories
}}
| This area was generated with Dilib version V0.6.33. |  |